\input macro.tex[let,jmc]
\ctrline{\bf FORMALIZATION OF TWO PUZZLES INVOLVING KNOWLEDGE}
\yyskip

	This paper describes a formal system and uses it to express the
puzzle of the three wise men and the puzzle of Mr. S and Mr. P.  Four
innovations in the axiomatization of knowledge were required: the
ability to express joint knowledge of several people, the ability to
express the initial non-knowledge, the ability to describe {\it knowing
what} rather than merely {\it knowing that}, and the ability to express
the change which occurs when someone learns something.  Our axioms are
written in first order logic and use Kripke-style possible worlds
directly rather than modal operators or imitations thereof.  We intend
to use functions imitating modal operators and taking ``propositions'' and
``individual concepts'' as operands, but we haven't yet solved the problem
of how to treat learning in such a formalism.

	The puzzles to be treated are the following:

\noindent {\bf The three wise men}

	{\it ``A certain king wishes to test his three wise men.  He
arranges them in a circle so that they can see and hear each other and tells
them that he will put a white or black spot on each of their foreheads
but that at least one spot will be white.  In fact all three spots
are white.  He then repeatedly asks them, ``Do you know the cclor of
your spot".  What do they answer?''}

	The solution is that they answer, {\it ``No''}, the first two
times the question is asked and answer {\it ``Yes''} thereafter.

	This is a variant form of the puzzle.  The traditional form
is

	{\it ``A certain king wishes to determine which of his three
wise men is the wisest.  He
arranges them in a circle so that they can see and hear each other and tells
them that he will put a white or black spot on each of their foreheads
but that at least one spot will be white.  In fact all three spots
are white.  He then offers his favor to the one who will first tell
him the color of his spot.  After a while, the wisest announces
that his spot his white.  How does he know?''}

	The intended solution is that the wisest reasons that if
his spot were black, the second would see a black and a white and
would reason that if his spot were black, the third would have seen
two black spot and reasoned from the king's announcement that his
spot was white.  This traditional version  requires
the wise men to reason about how fast their colleagues reason, and
we don't wish to try to formalize this.

\noindent {\bf Mr. S and Mr. P}

	{\it Two numbers $m$ and $n$ are chosen such that $2 ≤ m ≤ n ≤ 99$.
Mr. S is told their sum and Mr. P is told their product.  The following
dialogue ensues:}

\halign {\it Mr. P:	I don't know the numbers.\cr 
Mr. S:	I knew you didn't know.  I don't know either.\cr 

Mr. P:	Now I know the numbers.\cr 

Mr. S:	Now I know them too.\cr 

In view of the above dialogue, what are the numbers?\cr}

\yyskip
\noindent {\bf Simple axiomatization of the wise men}

	If we can assume that the first and second wisemen don't
know the colors of their spots, that the second knows that the
first doesn't know, and the third knows this, then a simple
axiomatization that doesn't explicitly treat learning works.

[In this paper, we omit this section.  Instead we include an
older self-contained memo written when this was our main approach
to the problem].

\yyskip
\noindent {\bf Full axiomatization of the wise men}

	The axioms are given in a form acceptable to FOL, the proof
checker computer program for an extended first order logic developed by
Richard Weyhrauch at the Stanford Artificial Intelligence Laboratory.
FOL uses a sorted logic and constants and variables are declared to have
given sorts, and quantifiers on these variables are interpreted as
ranging over the sorts corresponding to the variables.

	The axiomatization has the following features:

	\a . It is entirely in first order logic rather than in a modal
logic.

	\a . The Kripke accessibility relation is axiomatized.  No knowledge
operator or function is used.  We hope to present a second axiomatization
using a knowledge function, but we haven't yet decided how to handle time
and learning in such an axiomatization.

	\a . We are essentially treating ``knowing what'' rather than ``knowing
that''.  We say that $p$ knows the color of his spot in world $w$ by saying
that in all worlds accessible from $w$, the color of the spot is the same
as in $w$.

	\a . We treat learning by giving the accessibility relation a time
parameter.  To say that someone learns something is done by saying that
the worlds accessible to him at time $n+1$ are the subset of those accessible
at time $n$ in which the something is true.

	\a . The problems treated are complicated by the need to treat
joint knowledge and joint learning.  This is done by introducing
fictitious persons who know what a group of people know jointly.  (When
people know something jointly, not only do they all know it, but they
jointly know that they jointly know it).

\yyskip


This isn't the place for a description of the FOL interactive theorem
prover.  However a few remarks will make it easier to read the axioms.

	Since FOL uses a sorted logic, it must be told the sorts
of the variables and constants, so it can determine whether a substitution
is legitimate.  This is done by {\it declare} statements resembling
declarations in programming languages.  The notation for formulas in
as is usual in logic, so there shouldn't be difficulty reading it.
Writing it so that the computer will accept it is a more finicky task.

$$declare INDCONST RW ε WORLD;$$

declare INDVAR w w1 w2 w3 w4 w5 $ε$ WORLD;

\yskip
	$RW$ denotes the real world, and $w, w1, \ldots , w5$ are variables
ranging over worlds.

declare INDVAR m n m1 m2 m3 n1 n2 n3 $ε$ NATNUM;

	We use natural numbers for times.

\yskip

declare INDCONST S1 S2 S3 S123 $ε$ PERSON;

declare INDVAR p p0 p1 p2 $ε$ PERSON;

\yskip
	$S1$, $S2$ and $S3$ are the three wisemen.  $S123$
 is a fictitious person
who knows whatever $S1$, $S2$ and $S3$ know jointly.
  The joint knowledge of several
people is typified by events that occur in their joint presence.  Not only do
they all know it, but $S1$ knows that $S2$ knows that $S1$ knows that $S3$
 knows etc.
Instead of introducing $S123$, we could introduce prefixes of like ``$S1$
knows that $S2$ knows'' as objects and quantify over prefixes.

declare PREDCONST A(WORLD,WORLD,PERSON,NATNUM);

	This Kripke-style accessibility relation has two more arguments than
is usual in modal logic - a person and a time.

\yskip
declare INDVAR c c1 c2 c3 c4 $ε$ COLORS;

declare INDCONST W B $ε$ COLORS;

	There are two colors - white and black.

declare OPCONST color(PERSON,WORLD) = COLORS;

	A person has a color in a world.  A previous
axiomatization was simpler.  We merely had three propositions WISE1, WISE2
and WISE3 asserting that the respective wise men had white spots.  We now need
the colors, because we want to quantify over colors.

axiom reflex:	$∀w p m.A(w,w,p,m)$;;

	The accessibility relation is reflexive as is usual in the Kripke
semantics of M.  It is equivalent to asserting that what is known is true.

axiom transitive:	$∀w1 w2 w3 p m.(A(w1,w2,p,m)
 ∧ A(w2,w3,p,m) ⊃ A(w1,w3,p,m));;$

	Making the accessibility relation transitive gives an S4 like system.
We use transitivity in the proof, but we aren't sure it is necessary.

axiom who:	$∀p.(p=S1 ∨ p=S2 ∨ p=S3 ∨ p=S123);;$

	We need to delimit the set of wise men.

axiom w123:	$∀w1 w2 m.(A(w1,w2,S1,m) ∨ A(w1,w2,S2,m) ∨ A(w1,w2,S3,m)
⊃ A(w1,w2,S123,m));;$

	This says that anything the wise men know jointly, they
know individually.

axiom foolspot:	$∀w.(color(S123,w)=W);;$

	This ad hoc axiom is the penalty for introducing $S123$ as an
ordinary individual whose spot must therefore have a color.  It would have
been better to distinguish between real persons with spots and the
fictitious person(s) who only know things.  Anyway, we give $S123$ a white
spot and make it generally known, e.g. true in all possible worlds.  I must
confess that we do it this way here in order to repair a proof that the
computer didn't accept on account of people not knowing the color of
$S123$'s spot.

axiom color:	$¬(W=B)$

		$∀c.(c=W ∨ c=B)$

;;

	Both of these axioms about the colors are used in the proof.

axiom rw:	$color(S1,RW) = W ∧ color(S2,RW) = W ∧ color(S3,RW) = W;;$

	In fact all spots are white.

axiom king:	$∀w.(A(RW,w,S123,0) ⊃ color(S1,w)=W ∨ color(S2,w)=W
∨ color(S3,w)=W);;$

	They jointly know that at least one spot is white, since
the king stated it in their mutual presence.  We use the consequence
that S3 knows that S2 knows that S1 knows this fact.


axiom initial:	$∀c w.(A(RW,w,S123,0) ⊃
	(c=W ∨ color(S2,w)=W ∨ color(S3,w)=W
		⊃ ∃w1.(A(w,w1,S1,0) ∧ color(S1,w1) = c)) ∧
	(c=W ∨ color(S1,w)=W ∨ color(S3,w)=W
		⊃ ∃w1.(A(w,w1,S2,0) ∧ color(S2,w1) = c)) ∧
	(c=W ∨ color(S1,w)=W ∨ color(S2,w)=W
		⊃ ∃w1.(A(w,w1,S3,0) ∧ color(S3,w1) = c)))$

	$∀w w1.(A(RW,w,S123,0) ∧ A(w,w1,S1,0)
⊃ color(S2,w1) = color(S2,w) ∧ color(S3,w1) = color(S3,w))$

	$∀w w1.(A(RW,w,S123,0) ∧ A(w,w1,S2,0)
⊃ color(S1,w1) = color(S1,w) ∧ color(S3,w1) = color(S3,w))$

	$∀w w1.(A(RW,w,S123,0) ∧ A(w,w1,S3,0)
 color(S1,w1) = color(S1,w) ∧ color(S2,w1) = color(S2,w))$
;;

	These are actually four axioms.  The last three say that every one
knows that each knows the colors of the other men's spots.
The first part says that they all know that no-one knows anything
more than what he can see and what the king told them.  We establish
non-knowledge by asserting the existence of enough possible worlds.
The ability to quantify over colors is convenient for expressing this axiom
in a natural way.  In the S and P problem it is essential, because
we would otherwise need a conjunction of 4753 terms.

axiom elwek1:	$∀w.(A(RW,w,S123,1) ≡ A(RW,w,S123,0) ∧
∀p.(∀w1.(A(w,w1,p,0) ⊃ color(p,w1)=color(p,w)) ≡ ∀w1.(A(RW,w1,p,0)
⊃ color(p,w1)=color(p,RW))))$

	$∀w1 w2.(A(w1,w2,S1,1) ≡ A(w1,w2,S1,0) ∧ A(w1,w2,S123,1))$

	$∀w1 w2.(A(w1,w2,S2,1) ≡ A(w1,w2,S2,0) ∧ A(w1,w2,S123,1))$

	$∀w1 w2.(A(w1,w2,S3,1) ≡ A(w1,w2,S3,0) ∧ A(w1,w2,S123,1))$
;;

	This axiom and the next one are the same except that one
deals with the transition from time $0$ to time $1$ and the other deals
with the transition from time $1$ to time $2$.
Each says that
they jointly learn who (if anyone) knows the color of his spot.  The
quantifier $∀p$ in this axiom covers $S123$ also and forced us to say
that they jointly know the color of $S123$'s spot.

axiom elwek2:	$∀w.(A(RW,w,S123,2) ≡ A(RW,w,S123,1) ∧
∀p.(∀w1.(A(w,w1,p,1) ⊃ color(p,w1)=color(p,w)) ≡ ∀w1.(A(RW,w1,p,1)
⊃ color(p,w1)=color(p,RW))))$

	$∀w1 w2.(A(w1,w2,S1,2) ≡ A(w1,w2,S1,1) ∧ A(w1,w2,S123,1))$

	$∀w1 w2.(A(w1,w2,S2,2) ≡ A(w1,w2,S2,1) ∧ A(w1,w2,S123,1))$

	$∀w1 w2.(A(w1,w2,S3,2) ≡ A(w1,w2,S3,1) ∧ A(w1,w2,S123,1))$
;;

	The file WISEMA.PRF[S78,JMC] at the Stanford AI Lab contains
a computer checked proof from these axioms of

$$∀w.(A(RW,w,S3,2) ⊃ color(S3,w) = color(S3,RW))$$

which is the assertion that at time $2$, the third wise man knows the
color of his spot.  As intermediate results we had to prove that
previous to time $2$, the other wise men did not know the colors of
their spots.  In this symmetrical axiomatization, we could have proved
the theorem with a variable wise man instead of the constant $S3$.


\noindent {\bf Axiomatization of Mr. S and Mr. P}

	These axioms involve the same ideas as the wise man
axiomatization.  In fact, we derived them first.  The following modified
version of some axioms by Ma Xiwen of Peking University separates the
knowledge part of the problem from the arithmetic
part in a neat way.

Ma Xiwen's axioms for Mr. S and Mr. P which are a variant of an
earlier version by McCarthy.

 	 This is an approach to the axiomatization of Mr.S and Mr.P.
      	Its basic idea is the same of KNOW[E78,JMC].                  
	 These are some different symbols:
 
		k	for a PAIR of NATNUMs
		s(k)    for the sum of the two NATNUMs in k
		p(k)    for the product of the two NATNUMs in k
	
	 We have introduced a few of PREDCONSTs, for abbreviation only.
    	 But there are some important differences between the two 
	axiomatizations: our axiom SP is weaker, but our axioms LP
	and LS are stronger.
 	 The PREDCONSTs R1 R2 and R3 are slightly different,too.
	
	 Next follows a complete list of commands of the FOL proof of
	R3(k0). The subsequent proof that k0=<4,13> will be purely
	arithmetic, and a computer search has been done to confirm
	it.

	 


I have changed Ma's learning axioms LP and LS, and I have removed
the redundant predicate OK.  Where I have times 1 and 2 in
A(RW,w,SP,n), Ma had 0.  I think these axioms are too strong and
may even make the system inconsistent.  I don't know whether Ma's
proof will work with the weaker axioms.  - JMC



DECLARE INDVAR t ε NATNUM;
DECLARE INDCONST k0 ε PAIR;
DECLARE INDVAR k k1 k2 k3 ε PAIR;
DECLARE INDCONST RW ε WORLD;
DECLARE INDVAR w w1 w2 w3 ε WORLD;
DECLARE INDCONST S P SP ε PERSON;
DECLARE INDVAR r ε PERSON;
DECLARE OPCONST K(WORLD)=PAIR;  
DECLARE OPCONST s(PAIR)=NATNUM;
DECLARE OPCONST p(PAIR)=NATNUM;
DECLARE PREDCONST A(WORLD,WORLD,PERSON,NATNUM);

The predicates Qs, Qp, Q1, Q2, R1, R2 and R3 are represent
arithmetic conditions on the pair of numbers that are used to
express the arithmetic conditions on the pair that replace the
knowledge conditions given in the problem statement.

DECLARE PREDCONST Qs(PAIR) Qp(PAIR) Q1(PAIR) Q2(PAIR) Q3(PAIR);
DECLARE PREDCONST Bs(WORLD) Bp(WORLD) B1(WORLD) B2(WORLD);
DECLARE PREDCONST R1(PAIR) R2(PAIR) R3(PAIR);
DECLARE PREDCONST C1(WORLD) C2(WORLD);

The first two axioms state that the accessibility relation is
reflexive and transitive.  They assert that what is known is
true and one knows that one knows what one knows.  Got that?

AXIOM AR: ∀w r t.A(w,w,r,t);;
AXIOM AT: ∀w1 w2 w3 r t.(A(w1,w2,r,t)∧A(w2,w3,r,t)⊃A(w1,w3,r,t));;

This axiom says that the joint person knows what Mr. S and Mr. P
both know.  At first sight it seems too weak, but transitivity
tells us that what they jointly know, they jointly know they
jointly know.

AXIOM SP: ∀w1 w2 t.(A(w1,w2,S,t)∨A(w1,w2,P,t)⊃A(w1,w2,SP,t));;

This next axiom is just a definition for the purposes of abbreviation.
RW is the real world, so $k0$ is just the real pair.

AXIOM RW: k0=K(RW);;

In the initial situation they jointly know that Mr. S knows the sum
and Mr. P the product.  They also jointly know that this is all that
Mr. S and Mr. P know about the numbers.  This is asserted by saying
that given any pair of numbers with the right sum, there is a world
possible for Mr. S in which this is the pair of numbers.

AXIOM INIT:
    	∀w w1.(A(RW,w,SP,0)∧A(w,w1,S,0)⊃s(K(w))=s(K(w1))),
	∀w w1.(A(RW,w,SP,0)∧A(w,w1,P,0)⊃p(K(w))=p(K(w1))),
    	∀w k.(A(RW,w,SP,0)∧s(K(w))=s(k)⊃∃w1.(A(w,w1,S,0)∧k=K(w1))),
	∀w k.(A(RW,w,SP,0)∧p(K(w))=p(k)⊃∃w1.(A(w,w1,P,0)∧k=K(w1)));;

These axioms on the pair will be used to translate knowledge assertions.
For example, $Qs(k)$ asserts that there is another pair that has the
same sum as $k$ and is used in the assertion that Mr. S, knowing the
sum, does not know the pair, i.e. does not know the numbers.  As we
proceed through the dialog the arithmetic conditions become more
complex.

AXIOM QS: ∀k.(Qs(k)≡∃k1.(s(k)=s(k1)∧¬(k=k1)));;
AXIOM QP: ∀k.(Qp(k)≡∃k1.(p(k)=p(k1)∧¬(k=k1)));;
AXIOM Q:
	∀k.(Q1(k)≡∀k1.(s(k)=s(k1)⊃Qp(k1))),
	∀k.(Q2(k)≡∀k1.(R1(k1)∧p(k)=p(k1)⊃k=k1)),
	∀k.(Q3(k)≡∀k1.(R2(k1)∧s(k)=s(k1)⊃k=k1));;

AXIOM R:
	∀k.(R1(k)≡Qs(k)∧Q1(k)),
	∀k.(R2(k)≡R1(k)∧Q2(k)),
	∀k.(R3(k)≡R2(k)∧Q3(k));;

$BS(w)$ asserts that in the possible world $w$, Mr. S doesn't
know the numbers.

AXIOM BS: ∀w.(Bs(w)≡∃w1.(A(w,w1,S,0)∧¬(K(w)=K(w1))));;
AXIOM BP: ∀w.(Bp(w)≡∃w1.(A(w,w1,P,0)∧¬(K(w)=K(w1))));;
AXIOM B:
	∀w.(B1(w)≡∀w1.(A(w,w1,S,0)⊃Bp(w1))),
	∀w.(B2(w)≡∀w1.(A(w,w1,P,1)⊃K(w)=K(w1)));;
AXIOM C:
	∀w.(C1(w)≡Bs(w)∧B1(w)),
	∀w.(C2(w)≡C1(w)∧B2(w));;

The previous axioms were just definitions.  Now we have the
information coming from the dialog.  SKNPK stands for ``S Knows
that P does Not Know'' and the axiom asserts this about the
real world at time 0.

AXIOM SKNPK: B1(RW);;

NSK stands for ``S doesn't know'', and the axiom asserts this
about the real world.

AXIOM NSK:   Bs(RW);;

PK stands for ``P knows the numbers'', and the axiom asserts
this about the real world at time 1.

AXIOM PK:    B2(RW);;

SK tells us that at time 2, Mr. S knows the numbers.

AXIOM SK:    ∀w.(A(RW,w,S,2)⊃K(RW)=K(w));;

The last two axioms are the learning axioms.  LS tells us that
everyone learns by time 1 that Mr. S knew at time 0 that Mr. P
didn't know the numbers, and he didn't know them either.  LP
tells us that everyone learns by time 2 that Mr. P knew the
numbers by time 1.

AXIOM LP: ∀w w1.(A(RW,w,SP,1)⊃(A(w,w1,P,1)≡A(w,w1,P,0)∧C1(w1)));;
AXIOM LS: ∀w w1.(A(RW,w,SP,2)⊃(A(w,w1,S,2)≡A(w,w1,S,1)∧C2(w1)));;



The actual proof is carried out using a sequence of lemmas.
The first lemma shows the essential equivalence of a condition
on possible worlds with a condition on pairs.

COMMENT # LEMMA 1
	∀w k.(A(RW,w,SP,0)∧k=K(w)⊃(Qs(k)≡Bs(w))) 
COMMENT # LEMMA 2
        ∀w k.(A(RW,w,SP,0)∧k=K(w)→(Qp(k)≡Bp(w)))
COMMENT # LEMMA 3
	∀w k.(A(RW.w.SP,0)∧k=K(w)→(Q1(k)≡B1(w)))
COMMENT # LEMMA 4
	∀w k.(A(RW,w,SP,0)∧k=K(w)⊃(R1(k)≡C1(w)))
COMMENT # LEMMA 5
	R2(k0)
COMMENT # LEMMA 6
	∀w k.(A(RW,w,SP,0)∧k=K(w)⊃(R2(k)⊃C2(w)))
COMMENT # LEMMA 7
      	Q3(k0)
COMMENT # MAIN THEOREM
	R3(k0)

$R3(k0)$ is a purely arithmetic condition on the pair of numbers.
From an axiom asserting that $k0$ is a pair of numbers in the
interval $2 ≤ x ≤ 99$ and Peano's axioms for arithmetic, the numbers
can be proved to be 4 and 13.  Alternatively, $R3(k0)$ can be translated
into a computer program for computing the numbers.  Most people who
solve the problem write such a program.


\vfill\end